Nuprl Definition : non-void-decl
0,22
postcript
pdf
non-void(
d
) ==
x
dom(
d
).
A
=
d
(
x
)
A
latex
clarification:
non-void-decl(
T
;
eq
;
d
) == fpf-all(
T
;
eq
;
d
;
x
,
A
.
A
)
latex
Definitions
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
FDL editor aliases
non-void-decl
origin
x
dom(d). A=d(x) 
A
xdom(d). A=d(x) A
xdom(f). v=f(x) P(x;v)